Pgm, Sem:Type, equiv:(SemSemProp), X:(SemProp), S:(PgmSem), pr:Pgm, kpr:(SemPgm).
pr implements kpr  kpr |= X  pr |= X 

latex

Definitions	t  T, x:A. B(x), P  Q, pr |= X, pr implements kpr, kpr |= X, Prop
Lemmas	K-sem-sat wf, K-implements wf